fischer-delay{i:l,
fischer-delay{$x:ut2,
fischer-delay{$try:ut2,
fischer-delay{$taken:ut2,
fischer-delay{$contending:ut2,
fischer-delay{$free:ut2,
fischer-delay{$mine:ut2,
fischer-delay{$wanted:ut2,
fischer-delay{$z:ut2}
fischer-delay(es; del; L)
== e:es-E(es). 
== (loc(e)  L)
==  (((@e(mkid{$x:ut2}mkid{$try:ut2})  @e(mkid{$x:ut2}mkid{$taken:ut2}))
==  ( (((es-when(es; mkid{$x:ut2}; e) = mkid{$free:ut2})
==  (  (mkid{$x:ut2} unchanged-for del @ e))
==  (  ((es-when(es; mkid{$x:ut2}; e) = mkid{$contending:ut2})
==  (   (mkid{$x:ut2} unchanged-for 2 * del @ e))))
==   (@e(mkid{$x:ut2}mkid{$mine:ut2})  (mkid{$x:ut2} unchanged-for 2 * del @ e))
==   (((((es-when(es; mkid{$x:ut2}; e) = mkid{$contending:ut2})
==    (mkid{$x:ut2} unchanged-for 2 * del @ e))
==    ((es-when(es; mkid{$x:ut2}; e) = mkid{$free:ut2})  (mkid{$x:ut2} unchanged-for del @ e)))
==    ((es-isrcv(es; e))
==    c ((es-tag(es; e) = mkid{$wanted:ut2})
==    c  (i:Id. ((i  L)  (es-lnk(es; e) = <i, loc(e), mkid{$z:ut2}>))))))
==    @e(mkid{$x:ut2}mkid{$taken:ut2}))
==   ((es-isrcv(es; e))
==    ((es-tag(es; e) = mkid{$free:ut2})  (es-tag(es; e) = mkid{$wanted:ut2}))
==    (i:Id. ((i  L)  ((i = loc(e)))  (es-lnk(es; e) = <i, loc(e), mkid{$z:ut2}>)))
==    qless(es-time(es; e); (es-time(es; es-sender(es; e)) + del)))) 

latex

---

clarification:

fischer-delay{i:l,
fischer-delay{$x:ut2,
fischer-delay{$try:ut2,
fischer-delay{$taken:ut2,
fischer-delay{$contending:ut2,
fischer-delay{$free:ut2,
fischer-delay{$mine:ut2,
fischer-delay{$wanted:ut2,
fischer-delay{$z:ut2}
fischer-delay(es; del; L)
== e:es-E(es). 
== (es-loc(es; e)  L  Id)
==  (((es-change-to(es;Id;mkid{$x:ut2};e;mkid{$try:ut2})
==  ( es-change-to(es;Id;mkid{$x:ut2};e;mkid{$taken:ut2}))
==  ( (((es-when(es; mkid{$x:ut2}; e) = mkid{$free:ut2}  Id)
==  (  unchanged-for{i:l}
==  (  unchanged-for(Id; id-deq; es; mkid{$x:ut2}; del; e))
==  (  ((es-when(es; mkid{$x:ut2}; e) = mkid{$contending:ut2}  Id)
==  (   unchanged-for{i:l}
==  (   unchanged-for(Id; id-deq; es; mkid{$x:ut2}; (2 * del); e))))
==   (es-change-to(es;Id;mkid{$x:ut2};e;mkid{$mine:ut2})
==    unchanged-for{i:l}
==    unchanged-for(Id; id-deq; es; mkid{$x:ut2}; (2 * del); e))
==   (((((es-when(es; mkid{$x:ut2}; e) = mkid{$contending:ut2}  Id)
==    unchanged-for{i:l}
==    unchanged-for(Id; id-deq; es; mkid{$x:ut2}; (2 * del); e))
==    ((es-when(es; mkid{$x:ut2}; e) = mkid{$free:ut2}  Id)
==     unchanged-for{i:l}
==     unchanged-for(Id; id-deq; es; mkid{$x:ut2}; del; e)))
==    ((es-isrcv(es; e))
==    c ((es-tag(es; e) = mkid{$wanted:ut2}  Id)
==    c  (i:Id
==    c  (((i  L  Id)  (es-lnk(es; e) = <i, es-loc(es; e), mkid{$z:ut2}>  IdLnk))))))
==    es-change-to(es;Id;mkid{$x:ut2};e;mkid{$taken:ut2}))
==   ((es-isrcv(es; e))
==    ((es-tag(es; e) = mkid{$free:ut2}  Id)  (es-tag(es; e) = mkid{$wanted:ut2}  Id))
==    (i:Id
==    (((i  L  Id)
==    ( ((i = es-loc(es; e)  Id))
==    ( (es-lnk(es; e) = <i, es-loc(es; e), mkid{$z:ut2}>  IdLnk)))
==    qless(es-time(es; e); (es-time(es; es-sender(es; e)) + del)))) 

latex

Definitions	x:A. B(x), es-E(es), r * s, #$n, es-when(es; x; e), (x unchanged-for t @ e), id-deq, A c B, @e(xv), b, es-isrcv(es; e), P  Q, es-tag(es; e), P  Q, x:A. B(x), (x  l), P  Q, A, Id, s = t, IdLnk, es-lnk(es; e), <a, b>, loc(e), mkid{$x:ut2}, qless(r; s), r + s, es-time(es; e), es-sender(es; e)
FDL editor aliases	fischer-delay